Electronic circuits, such as integrated microcircuits, are used in a variety of products, from automobiles to microwaves to personal computers. Designing and fabricating microcircuit devices typically involves many steps, sometimes referred to as the “design flow.” The particular steps of a design flow often are dependent upon the type of microcircuit, its complexity, the design team, and the microcircuit fabricator or foundry that will manufacture the microcircuit. Typically, software and hardware “tools” verify the design at various stages of the design flow by running software simulators and/or hardware emulators. These steps aid in the discovery of errors in the design, and allow the designers and engineers to correct or otherwise improve the design. These various microcircuits are often referred to as integrated circuits (IC's).
Several steps are common to most design flows. Initially, the specification for a new circuit is transformed into a logical design, sometimes referred to as a register transfer level (RTL) description of the circuit. With this logical design, the circuit is described in terms of both the exchange of signals between hardware registers and the logical operations that are performed on those signals. The logical design typically employs a Hardware Design Language (HDL), such as the Very high speed integrated circuit Hardware Design Language (VHDL). The logic of the circuit is then analyzed, to confirm that it will accurately perform the functions desired for the circuit. This analysis is sometimes referred to as “functional verification.”
After the accuracy of the logical design is confirmed, it is converted into a device design by synthesis software. The device design, which is typically in the form of a schematic or netlist, describes the specific electronic devices (such as transistors, resistors, and capacitors) that will be used in the circuit, along with their interconnections. This device design generally corresponds to the level of representation displayed in conventional circuit diagrams. The relationships between the electronic devices are then analyzed, often mathematically, to confirm that the circuit described by the device design will correctly perform the desired functions. This analysis is sometimes referred to as “formal verification.” Additionally, timing verifications are often made at this stage, by for example simulating the various clocks employed to drive the device.
Once the components and their interconnections are established, the design is again transformed, this time into a physical design that describes specific geometric elements. This type of design often is referred to as a “layout” design. The geometric elements, which typically are polygons, define the shapes that will be created in various layers of material to manufacture the circuit. Typically, a designer will select groups of geometric elements representing circuit device components (e.g., contacts, channels, gates, etc.) and place them in a design area. These groups of geometric elements may be custom designed, selected from a library of previously-created designs, or some combination of both. Lines are then routed between the geometric elements, which will form the wiring used to interconnect the electronic devices. Layout tools (often referred to as “place and route” tools), such as Mentor Graphics' IC Station or Cadence's Virtuoso, are commonly used for both of these tasks.
As indicated, device verification often takes place prior to the actual manufacturing of the device. As a result, hardware description languages are typically employed to model the hardware and act as an embodiment for testing purposes. However, testing and verification of physical devices also occurs after manufacturing. For purposes of brevity and clarity, a distinction between verification at the design level and at the physical level is not always made in the balance of this disclosure. Furthermore, the term device may be used interchangeably to refer to a physical embodiment of the device as well as to models or representations of the device.
Clock Domain Crossing Verification
As stated, verification of the timing of a device often takes place during device development. The speed with which components in a circuit process signals is dictated or “driven” by a clock. Modern circuits may have multiple clocks. For example, a modern microprocessor may have a clock that allows for performance at maximum speed as well as a second clock that allows the device to perform at a reduced speed. Due to the flexibility of modern designs, multiple clocks are often required. The number of clocks in a given design is further increased by the fact that modern circuits are decreasing in size exponentially, which has allowed designers to add an increased number of circuit components into a design of a given size. This is especially true in the realm of System-on-Chip (SOC) devices.
A System-on-Chip is a microcircuit device that contains blocks or “systems” for performing various tasks, packaged as a single device. System-on-Chip devices are prevalent in modern electronics, such as cell-phones, digital video disk (DVD) players, video game consoles, household appliances, automobiles, and telecommunications equipment. Typically, a System-on-Chip is composed of blocks specifically designed to perform a particular task. These blocks are all interconnected by some communication structure, such as a shared communication bus or even a Network-on-Chip (NoC).
The components or blocks of a circuit are driven by a particular clock or a particular clock frequency. A clock having a particular frequency or speed is often referred to as a clock domain. More particularly, a clock domain is a circuit component or group of components driven by a clock or even a group of clocks that have a fixed phase relationship to each other. Clocks that are asynchronous to each other belong to different clock domains. Similarly, components driven by asynchronous clocks are said to belong to different clock domains.
Electronic signals may originate from one clock domains and be conveyed or transferred to a different clock domain, by for example signal sampling. A signal that originates in a different clock domain than it is received is said to be a clock domain crossing (CDC) signal. Designs where multiple clock domain crossings occur have historically been difficult for designers to verify. Compounding this verification problem is the fact that modern devices, such as system on chips, may contain dozens of clock domains and approximately 104 clock domain crossing signals.
One of the problems associated with clock domain crossings is metastability. Metastability is discussed in an article by C. Cumming entitled “Synthesis and Scripting Techniques for Designing Multi-Asynchronous Clock Designs,” published by Synopsis Users Group (SNUG) in 2001, which article is incorporated entirely herein by reference. Metastability occurs when, for example, the data stored within a memory storage register changes during either the setup time or the hold time of the register.
Historically, metastability was countered by adding synchronizers at the clock domain crossing boundaries. For example, two back-to-back flip-flops may be employed as synchronizers. This synchronizer scheme, however, does not prevent random delay from being introduced into the receiving clock domain. Some other common approaches to resolving clock domain crossings are to employ a first in first out (FIFO) data abstraction scheme or to employ a handshaking scheme.
Various other schemes for resolving and verifying clock domain crossings are discussed in “A Methodology for Verifying Sequential Reconvergence of Clock-Domain Crossing Signals,” by T. Ly et al., Design and Verification Conference, 2005, “Symbolic Model Checking Without BDDs,” by A. Biere et al., Fifth International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99), pp. 193-207, March 1999, “Symbolic Model Checking,” by K. L. McMillan, Kluwer Academic Publishers, Boston Mass., 1994, “Computer-Aided Verification of Coordinating Processes,” by R. P. Kurshan, Princeton University Press, Princeton N.J., 1994, “Clock Domain Crossing-Closing the Loop on Clock Domain Function Implementation Problems,” Cadence Design Systems, 2004, “The Need for an Automated Clock domain crossing verification Solution,” by N. Hand, Mentor Graphics Corporation, 2006, “Critical Clock-Domain-Crossing Bugs,” by S. Sarwary et al., Electronics Design Strategy News, Apr. 3, 2008, “Formal Verification of Synchronizers,” by T. Kapschitz et al., Conference of Correct Hardware Design and Verification Methods, 2005, “Using Assertion-Based Verification to Verify Clock Domain Crossing Signals,” by C. Kwok et al., Design and Verification Conference, 2003, and “Verifying Synchronization in Multi-Clock Domain SoC,” by T. Kapschtiz et al., Design and Verification Conference, 2004, which articles are all incorporated entirely herein by reference.
The above methods for dealing with clock domain crossings fail to provide a complete framework for resolving and verifying clock domain crossings. For example, the above clock domain crossing verification methods lack procedures for on the fly analysis and procedures for structural analysis. An additional limitation with conventional formal verification methods is due to their limited capacity. As a result, most conventional formal verification methods operate on the block level of verification. This is significantly different from the other functional verification methods, which execute over the entire circuit.
An additional limitation with conventional formal verification methods is that the methods do not operate automatically. That is to say that a user must manually configure the design and feed any verification assertions generated from the various clock domain crossing tools into any necessary simulation or formal verification tools. This drawback is extremely inconvenient and adds significantly to the time required for verification.
Further limitation with conventional formal verification methods result from their performing verification after the signal has crossed the clock domain. For example, some methods collect all the checks and assertions during a clock domain crossing analysis, and then synthesize them together with the design to form a formal netlist, and finally perform formal verification on the synthesized netlist. This approach is not ideal, however, as most clock domain crossing protocols are not local and require a flattened synthesized design. More particularly, the checks ensure that data and control signals are correctly conveyed across clock domain crossings. Although formal techniques, such as abstraction refinement, are efficient techniques to verify local properties like clock domain crossings, they must operate on bit-level or word-level netlists. As a result of this restriction, memory consumption issues may prevent a clock domain crossing verification from being performed on a particular device.